;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;CS 710 - AI - Program 3 - Fall 2012
;Author: Justin J. Ploegert (ploegert@uwm.edu)
;p3-testfun.lisp
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


;====================================================================================================
; Part D Functions

(defun load-start-states (sentence )
  "Loads the start states for the STRIPS operator"
  (dolist (i sentence)
    (write-line (format nil "(part_d ~A ~A)" i (wfp-checkerFOL i)))
  ))


(defun load-goal-states (sentence )
  "Loads the goal states for the STRIPS operator"
  (dolist (i sentence)
    (write-line (format nil "(part_d ~A ~A)" i (wfp-checkerFOL i)))
  ))


(defun load-operators (sentence )
  "Loads the operators for the STRIPS operator"
  (dolist (i sentence)
    (dolist (x i)
      (write-line (format nil "(part_d ~A ~A)" x (wfp-checkerFOL x)))
      )
  ))



(defun part_a (sentence)
  "Runs the tests for Part A"
  (dolist (i sentence)
    (write-line (format nil "(part_a ~A ~A)" i (wfp-checker i)))
  ))

(defun part_b (sentence interpretation)
  "Runs the tests for Part b"
  ;(write-line (format nil "interpretation ~A" interpretation ))
  ;(write-line (format nil "-----------------------------------"))
  (dolist (i sentence)
    (write-line (format nil "(part_b ~A ~A)" i (TruthValue  i interpretation)))
    ))

(defun part_b_tautology (sentence)
  "Runs the tests for the tautology portion of part b"
  (dolist (i sentence)
  ;(write-line (format nil "(part_a ~A ~A)" sentence (wfp-checker sentence)))
  ;(write-line (format nil "(part_b ~A ~A)" i (TruthValue  i)))
  (write-line (format nil "(part_b ~A ~A)" i (IsTautology i)))
  ))

(defun part_c (sentence)
  "Runs the test for part c"
  (dolist (i sentence)
  ;(write-line (format nil "(part_c ~A ~A)" sentence (wfp-checker sentence)))
  (write-line (format nil "(part_c ~A ~A)" i (wfp-checkerFOL i)))
  ))

(defun part_d ()
    
;======================================
;Initial State:
  (setf start-state
  '((S |a| |u|)         ;(side cat left)
    (S |b| |u|)         ;(side rat left)
    (S |c| |u|)         ;(side grain left)
    (S |d| |u|)         ;(side farmer left)
    (S |e| |u|)         ;(side boat left)
))

;======================================
;Initial State:
  (setf goal-state
  '((S |a| |v|)         ;(side cat right)
    (S |b| |v|)         ;(side rat right)
    (S |c| |v|)         ;(side grain right)
    (S |d| |v|)         ;(side farmer right)
    (S |e| |v|)         ;(side boat right)
))
  



;======================================
;Operators
  (setf operators
  '(
    ;ACTION
    ((F)                   ; (boatfull)
    ;PRECOND
    (AND (I |d|) (OR (AND (I |a|) (I |b|))    ; (and (inboat farmer) (or (and (inboat cat) (inboat rat)
                    (AND (I |c|) (I |b|))    ;                          (and (inboat grain) (inboat rat))
                    (AND (I |c|) (I |a|)))) ;                          (and (inboat grain) (inboat)))))
    ;ADD
    ((F))                  ; (boatfull) - The Boat is full
    ;DELETE
    ((N)))                 ; (boatnotfull) - The boat is not full

    ;ACTION
    ((M |x|)                 ; (moveboat) - move boat to x side
    ;PRECOND
    (AND (S |e| |y|) (J |d|))  ; ((side boat Y) (inboat farmer))
    ;ADD
    ((S |e| |x|))              ;  ((side boat X))
    ;DELETE
    ((S |e| |y|)))       ; ((side boat y)))
    
    ;ACTION
    ((U |x| |y|)          ; (unload X Y)    - unload x item on y side
    ;PRECOND
    (AND (S |e| |y|) (I |x|))    ; (side boat Y) (inboat X))
    ;ADD
    ((S |x| |y|))              ; (side X Y))
    ;DELETE
    ((I |x|) (N)))           ; ((I X) (boatnotfull)))

    ;ACTION
    ((L |x| |y|)               ; load X Y) - unload x item from y side
    ;PRECOND
    (AND (S |e| |y|) (S |x| |y|))  ; (side boat Y) (side X Y))
    ;ADD
    ((I |x|))                ; ((I X))
    ;DELETE
    ((S |x| |y|)))             ; ((side X Y)))

    ;ACTION
    ((E |a| |b| |z|)      ; (eats cat rat z) - cat eats rat  on Z side if farmer is not on Z side
    ;PRECOND
    (AND (S |d| |y|) (S |a| |z|) (S |b| |z|))     ; (side farmer Y) (side X Z) (size Y Z))
    ;ADD
    (())
    ;DELETE
    ((S |b| |z|)))  ; side Y Z)) - Y is eaten, and therefore on no side. you will never reach goal becuase Y is missing.
))

  
  (write-line (format nil "Representation"))
  (write-line (format nil "============================"))
  (write-line (format nil "Constants: "))
  (write-line (format nil "|a| - cat"))
  (write-line (format nil "|b| - rat"))
  (write-line (format nil "|c| - grain"))
  (write-line (format nil "|d| - farmer"))
  (write-line (format nil "|e| - boat"))
  
  (write-line (format nil "|u| = left"))
  (write-line (format nil "|v| = right"))
  (write-line (format nil "Predicates"))
  (write-line (format nil "S = side"))
  (write-line (format nil "M = moveboat"))
  (write-line (format nil "F = boatfull"))
  (write-line (format nil "N = boatnotful"))
  (write-line (format nil "I = inboat"))
  (write-line (format nil "L = load"))
  (write-line (format nil "U = unload"))
  (write-line (format nil "E = eats"))      
  
  
  ;Start Calls
  (write-line (format nil "Start-State:~a" start-state))
  (dolist (i start-state)
    (write-line (format nil "(start-state: ~a)" i )))
  
  (write-line (format nil "Goal-State:~a" goal-state))
  (dolist (i start-state)
    (write-line (format nil "(goal-state: ~a)" i )))
  
  (write-line (format nil "The Plan!"))
  (write-line (format nil "============================"))
  (write-line (format nil "(L |b|) ==> (load rat)"))
  (write-line (format nil "(L |d|) ==> (load farmer)"))
  (write-line (format nil "(M |v|) ==> (moveboat left)"))
  (write-line (format nil "(U |d|) ==> (unload farmer)"))
  (write-line (format nil "(U |b|) ==> (unload rat)"))
  (write-line (format nil "(L |d|) ==> (load farmer)"))
  (write-line (format nil "(M |v|) ==> (moveboat left)"))
  (write-line (format nil "(U |d|) ==> (unload farmer)"))
  (write-line (format nil "(L |c|) ==> (load grain)"))
  (write-line (format nil "(L |d|) ==> (load farmer)"))
  (write-line (format nil "(M |v|) ==> (moveboat right"))
  (write-line (format nil "(U |d|) ==> (unload farmer)"))
  (write-line (format nil "(U |c|) ==> (unload grain)"))
  (write-line (format nil "(L |b|) ==> (load rat)"))
  (write-line (format nil "(L |d|) ==> (load farmer)"))
  (write-line (format nil "(M |u|) ==> (moveboat left)"))
  (write-line (format nil "(U |d|) ==> (unload farmer)"))
  (write-line (format nil "(L |a|) ==> (load cat)"))
  (write-line (format nil "(L |d|) ==> (load farmer)"))
  (write-line (format nil "(M |v|) ==> (moveboat right)"))
  (write-line (format nil "(U |a|) ==> (unload cat)"))
  (write-line (format nil "(U |d|) ==> (unload farmer)"))
  (write-line (format nil "(U |b|) ==> (unload rat)"))
  
  
  (write-line (format nil "Operators:"))
  (dolist (i operators)
    (write-line (format nil "(New Action)"))
    (dolist (x i)
      (write-line (format nil "(Ops ~A)" x ))
      )
    
    (setf the-plan '(((L |b|) (L |d|) (M |v|) (U |d|) (U |b|) (L |d|)
(M |v|) (U |d|) (L |c|) (L |d|) (M |v|) (U |d|) (U |c|) (L |b|)
(L |d|) (M |u|) (U |d|) (L |a|) (L |d|) (M |v|) (U |a|) (U |d|) (U |b|))))
      
))

;====================================================================================================


(defun parta-tests ()
  "Unit Tests for part_A"
  (write-line (format nil "============================"))
  (write-line (format nil "Running tests for part a...- WFP-CHECKER"))
  (write-line (format nil "============================"))
  
  ; should pass
  (case? "BOB")
  (case? "B12")
  (case? "P")
  (case? "John is up")

  
  ; should fail
  (case? "p")
  (case? "B12B")
  (case? "a12")
  (case? "123")
  (case? "John is up")
  
  ; should fail
  (write-line (format nil "These should fail..."))
  (wfp-checker '(f f f))
  (wfp-checker '(john is up))
  (wfp-checker 'p)
  (wfp-checker '(p q))
  (wfp-checker '(AND (OR P (NOT Q)) (OR (NOT P) Q)))
  (wfp-checker '(NOT P))
  (wfp-checker '(IMPLIES P (Q)))
  (wfp-checker '(IMPLIES (P) Q))
  (wfp-checker '(EQUIV (P) Q))
  (wfp-checker '(EQUIV P (Q)))
  (wfp-checker '(|p|))
  ;Should Pass
  (write-line (format nil "These should pass.."))
  (wfp-checker '(P))
  (wfp-checker '(|P|))
  (wfp-checker '("John is up"))
  (wfp-checker '(NOT (P)))
  (wfp-checker '(IMPLIES (P) (Q)))
  (wfp-checker '(EQUIV (P) (Q)))
  (wfp-checker '(AND (OR (P) (NOT (Q))) (OR (NOT (P)) (Q))))  
  
  (part_a '((f f f) (john is up) p (p q) (AND (OR P (NOT Q)) (OR (NOT P) Q)) (NOT P) (IMPLIES P (Q)) (IMPLIES (P) Q) (EQUIV (P) Q) (EQUIV P (Q)) (|p|)))
  (part_a '((P) (|P|) ("John is up") (NOT (P)) (IMPLIES (P) (Q)) (EQUIV (P) (Q)) (AND (OR (P) (NOT (Q))) (OR (NOT (P)) (Q)))))
  
)


(defun partb-tests ()
  (write-line (format nil "============================"))
  (write-line (format nil "Running Unit tests for part b...- TruthValue and isTautology"))
  (write-line (format nil "============================"))
  "Unit Tests for part_B"
  ;Should Fail
  
  
  (IsTautology '(OR (P) (NOT (P))))
  (IsTautology '(IMPLIES (P) (Q)))
  (IsTautology '(and (P) (Q)))
  (IsTautology '(EQUIV (P) (Q)))
  (IsTautology '(EQUIV (IMPLIES (P)(Q)) (OR (NOT (P))(Q))))
  
  
  (setf interpretation '((P nil) (Q nil) (P1 t) (P2 nil) (Q3 t) (P4 nil) (P5 t) (Q6 nil)))
  (setf sentence '((NOT (P))))
  (write-line (format nil "Sentence is: ~a" sentence))
  (write-line (format nil "Interpretation is: ~a" interpretation))
  (part_b sentence interpretation)
  
  (setf sentence '((AND (P)(Q))))
  (write-line (format nil "Sentence is: ~a" sentence))
  (write-line (format nil "Interpretation is: ~a" interpretation))
  (part_b sentence interpretation)
  
  
  (setf sentence '((OR (AND) (P)(Q)) (OR (P)(Q))))
  (write-line (format nil "Sentence is: ~a" sentence))
  (write-line (format nil "Interpretation is: ~a" interpretation))
  (part_b sentence interpretation)
  
  (setf sentence '((NOT (P)) (AND (P)(Q)) (OR (P)(Q)) (IMPLIES (P)(Q)) (EQUIV (P)(Q)) 
                   (EQUIV (IMPLIES (P1) (AND (P2) (Q3))) (NOT (OR (P4) (IMPLIES (P5)(Q6)))))
                   (IMPLIES (P)(P)) (EQUIV (IMPLIES (P)(Q)) (OR (NOT (P))(Q))) (EQUIV (NOT   
                   (AND (P)(Q))) (OR (NOT (P))(NOT (Q)))) (IMPLIES (P) (IMPLIES (Q)(P))) (OR
                                                                                                                                                              (P) (NOT (P)))))
  
  (write-line (format nil "Sentence is: ~a" sentence))
  (write-line (format nil "Interpretation is: ~a" interpretation))
  (part_b sentence interpretation)
  
  (setf interpretation '((P t) (Q t) (P1 t) (P2 nil) (Q3 t) (P4 nil) (P5 t) (Q6 nil)))
  (setf sentence '((NOT (P))))
  (write-line (format nil "Sentence is: ~a" sentence))
  (write-line (format nil "Interpretation is: ~a" interpretation))
  (part_b sentence interpretation)
  
  (setf sentence '((AND (P)(Q))))
  (write-line (format nil "Sentence is: ~a" sentence))
  (write-line (format nil "Interpretation is: ~a" interpretation))
  (part_b sentence interpretation)
  
  
  (setf sentence '((OR (AND) (P)(Q)) (OR (P)(Q))))
  (write-line (format nil "Sentence is: ~a" sentence))
  (write-line (format nil "Interpretation is: ~a" interpretation))
  (part_b sentence interpretation)
  
  (setf sentence '((NOT (P)) (AND (P)(Q)) (OR (P)(Q)) (IMPLIES (P)(Q)) (EQUIV (P)(Q)) 
                   (EQUIV (IMPLIES (P1) (AND (P2) (Q3))) (NOT (OR (P4) (IMPLIES (P5)(Q6)))))
                   (IMPLIES (P)(P)) (EQUIV (IMPLIES (P)(Q)) (OR (NOT (P))(Q))) (EQUIV (NOT   
                   (AND (P)(Q))) (OR (NOT (P))(NOT (Q)))) (IMPLIES (P) (IMPLIES (Q)(P))) (OR
                   (P) (NOT (P)))))
  (write-line (format nil "Sentence is: ~a" sentence))
  (write-line (format nil "Interpretation is: ~a" interpretation))
  (part_b sentence interpretation)
  
  (setf sentence '((NOT (P)) (AND (P)(Q)) (OR (P)(Q)) (IMPLIES (P)(Q)) (EQUIV (P)(Q)) 
    (EQUIV (IMPLIES (P1) (AND (P2) (Q3))) (NOT (OR (P4) (IMPLIES (P5)(Q6)))))
    (IMPLIES (P)(P)) (EQUIV (IMPLIES (P)(Q)) (OR (NOT (P))(Q))) (EQUIV (NOT   
    (AND (P)(Q))) (OR (NOT (P))(NOT (Q)))) (IMPLIES (P) (IMPLIES (Q)(P))) (OR
    (P) (NOT (P)))))

  (write-line (format nil "Sentence is: ~a" sentence))
  (write-line (format nil "Interpretation is: ~a" interpretation))
  (part_b_tautology sentence)
  
)




(defun partc-tests ()
  "Unit Tests for part_C"
  
  (write-line (format nil "============================"))
  (write-line (format nil "Running UNIT tests for part a...- WFP-CHECKERFOL"))
  (write-line (format nil "============================"))
  
  ;Should Pass
  (part_c '((P)))
  (part_c '((P |a|)))
  (part_c '((P |x|)))
  (part_c '((P |a| |b|)))
  (part_c '((AND (I |x|) (P |y|))))
  (part_c '((AND (S |e| |y|) (I |d|))))
  (part_c '((P |a| |b| |c|)))
  (part_c '((P (|f| |a|))))
  (part_c '((P (|f| |a| |b|))))
  (part_c '((P (|a| |b|))))
  (part_c '((P (|f| |a|))))
  (part_c '((NOT (P |x|))))
  (part_c '((NOT (P |x| |y| |z|))))
  (part_c '((NOT (P |a| |b| |z|))))
  (part_c '((OR (P |x| |y| |z|))))
  (part_c '((OR(P |a| ) (Q |b| ))))
  (part_c '((OR (P))))
  (part_c '((IMPLIES (P |a| ) (Q |b| ))))
  (part_c '((EQUIV (P |a| ) (Q |b| ))))
  (part_c '((ALL |v| (P |v|(|f| |v|)))))
  (part_c '((ALL |x| |y| (P |x| |y|))))
  (part_c '((EXISTS |v| ( P |v|(|f| |v|)))))
  
  (part_c '((IMPLIES (Q |u| (|f| |a| |v|) |d|) (R (|g| (|h| |b| |c| |w|)) |y|))))
  (part_c '((AND (S |e| |y|) (J |d|))))
  
  ;Should Fail
  (part_c '((P |f|)))
  (part_c '((P |a| |f|)))
  (part_c '((P (|a| |f|))))
  (part_c '((IMPLIES (NOT (OR (P |a|) (Q |b|)))  Q |c|)))
  
  (term-type "a")
  (term-type "f")
  (term-type "v")
  (term-type "A")
  
  (termp "a")
  (termp "f")
  (termp "v")
  (termp "P")
  (predicatep "a")
  (predicatep "f")
  (predicatep "v")
  (predicatep "P")
  (funcp "a")
  (funcp "f")
  (funcp "v")
  (funcp "P")
  
  (part_c '((NOT (P |x| |y| |z|)) (P (|f| |b| |y|) |y|) 
           (IMPLIES (Q |u| (|f| |a| |v|) |d|) (R (|g| (|h| |b| |c| |w|)) |y|)) 
           (ALL |x| (IMPLIES (A |x| |c|) (B |x| |d|))) 
           (ALL |x| (EXISTS |y| (IMPLIES (A |y|) (B |x|)))) 
           (AND (ALL |x| (P |x|)) (Q |y| |z|)) 
           (EQUIV (B |f| |u| |a|) (P ())) (P |x| |a| Q)
           (ALL |x| |y| (P |x| |y|)) (ALL |x| (IMPLIES (A |y| |c|) (B |x| |d|))) 
           (ALL |z| (EXISTS |y| (IMPLIES (A |y|) (B |x|))))))
  )